Problem:
 f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v))
 f(x,y,y) -> y
 f(x,y,g(y)) -> x
 f(x,x,y) -> x
 f(g(x),x,y) -> y

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {3,2}
   transitions:
    f0(1,1,1) -> 2*
    f0(1,3,1) -> 2*
    f0(3,1,1) -> 2*
    f0(3,3,1) -> 2*
    f0(1,1,3) -> 2*
    f0(1,3,3) -> 2*
    f0(3,1,3) -> 2*
    f0(3,3,3) -> 2*
    g0(1) -> 3*,2,1
    g0(3) -> 2,3*
    1 -> 2*
    3 -> 2*
  problem:
   
  Qed